\section{Skolemov tvar formuly}

\begin{definicia}[Skolemov normálny tvar]$\!\!\!$\footnote{Pozn.:
    Táto definícia sa mierne líši od štandardnej, v tej sa nemôžu
    vyskytovať žiadne existenčné kvantifikátory
    }
  Uvažujme uzevretú formulu $A$.
  Ak $A$ má prefix $(\exists x_1)(\exists x_2) \dots (\exists x_k)
    (\forall x_{k+1}) (\forall x_{k+2}) \dots (\forall x_n)$, potom 
    hovoríme, že formula $A$ je vyjadrená v Skolemovom normálnom
    tvare, pričom $0 \le k \le n$.
\end{definicia}

\begin{veta}
    Nech $A$ je formula predikátovej logiky. Potom k nej môžeme
    zostrojiť formulu $A'$ v Skolemovom normálnom tvare, pričom platí
    $\provable A \iff \provable A'$.
    \label{veta:skolem}
\end{veta}

\begin{poznamka}
    Všimnime si, že predchádzajúca veta nehovorí nič o existencii
    formuly $A'$ takej, že $\provable A \lequiv A'$ ako to
    bolo u prenexného tvaru. Taká formula totiž v prípade Skolemovho
    normálneho tvaru nemusí existovať.
\end{poznamka}

\begin{definicia}[Hodnosť formuly]
    Uvažujme formulu $A$ vyjadrenú v prenexnom tvare. Potom pod
    hodnosťou formuly $A$ označíme počet veľkých kvantifikátorov,
    ktoré v prefixe predchádzajú \emph{posledný} existenčný
    kvantifikátor (počítame zľava doprava).
\end{definicia}

\begin{priklad}
    Uvažujme formulu
    \begin{equation*}
        \highlighta{(\forall x) (\forall y)}
        (\exists z) 
        \highlighta{(\forall u)}
        (\exists w)
        \highlightc{(\exists v)}
        (\forall s) (\forall t) A
    \end{equation*}
    Jej hodnosť je 3.
\end{priklad}

\def\existsxton{(\exists x_1) (\exists x_2) \dots (\exists x_n)}
\def\forallxton{(\forall x_1) (\forall x_2) \dots (\forall x_n)}

\begin{dokaz}[Vety \ref{veta:skolem} o Skolemovom tvare]
%%% {{{
    Budeme predpokladať, že $A$ je uzavretá 
    (Podľa vety o uzávere
    platí, že je dokázateľné $\provable A$ práve vtedy,
    keď je dokázateľný uzáver formuly $A$)
    a taktiež že je v prenexnom tvare (to vieme zabezpečiť).
    Dôkaz bude prebiehať matematickou indukciou vzhľadom na hodnosť
    $m$ formuly $A$.
    \begin{itemize}
        \item $m=0$ - $A$ je v Skolemovom normálnom tvare
        \item IP: tvrdenie vety platí pre každú
        formulu ktorej hodnosť je $m-1$.
        Nech je teda $A$ tvaru
        \begin{equation}
            A: \existsxton (\forall y) B(x_1,x_2,\dots,x_n,y)
        \end{equation}
        kde $B$ \emph{nie je} nutne bezkvantifikátorová (a je v
        prenexnom tvare).
        Pretože $A$ je uzavretá, v $B$ sú voľné iba $x_1,x_2,\dots,x_n,y$.
        Keďže hodnosť $A$ je $m$, tak vo formule $B$ poslednému
        existenčnému kvantifikátoru predchádza práve $m-1$ všeobecných
        kvantifikátorov.
        Nech $P^{n+1}$ je $(n+1)$-árny predikát, ktorý sa nevyskytuje v
        $A$ (a teda ani $B$). Uvažujme nasledujúcu formulu
        \begin{equation}
            A^*: \existsxton \left[
                (\forall y) [B(x_1,\dots,x_n,y) \implies 
                    P^{(n+1)}(x_1,\dots,x_n,y)] \implies 
                    (\forall y) P^{(n+1)} (x_1,\dots,x_n,y)
            \right]
        \end{equation}
        Postupne ukážeme, že $\provable A \iff \; \provable
        A^*$.
        %%% {{{ \provable A <==> \provable A*
        \begin{itemize}
        \item[$\Rightarrow$]
        %%% {{{ ==>
            \begin{itemize}
            \item[0] $\provable A$

            \item[1] $\provable \highlightb{(B \implies P^{(n+1)}) \implies
                            (B \implies P^{(n+1)})}$ -- inštancia
                            $X\implies X$.

            \item[2] $\provable (X\implies (Y\implies Z)) \implies
                            (Y\implies (X\implies Z))$ -- veta o zámene
                            predpokladov

            \item[3] $\provable 
                \highlightb{[\underbrace{(B \implies P^{(n+1)})}_{X} \implies 
                        (\underbrace{B}_{Y} \implies
                        \underbrace{P^{(n+1)}}_{Z}))]} \implies
                \highlighta{[ \underbrace{B}_{Y} \implies
                 (\underbrace{(B \implies P^{(n+1)})}_{X} \implies
                        \underbrace{P^{(n+1)}}_{Z})]}$ -- inštancia
                        kroku 2

            \item[4] $\provable
                 \highlighta{B \implies
                 ((B \implies P^{(n+1)}) \implies
                        P^{(n+1)})}$ -- MP 1,3.\footnote{
                        Toman: Ideme to obliecť, zatiaľ je
                        obnažená.}

            \item[x] $\provable \highlightc{\highlighto{(\forall y)}
                B} \implies \highlightp{\highlighto{(\forall y)}(
                (B \implies P^{(n+1)}) \implies P^{(n+1)})}$ --
                veta o distribúcii kvantifikátorov aplikovaná na
                4

            \item[y] $\highlightp{(\forall y)(
                (B \implies P^{(n+1)}) \implies P^{(n+1)})}
                \implies
                \highlightb{(\highlighto{(\forall y)}(B \implies P^{(n+1)}) 
                    \implies
                     \highlighto{(\forall y)}P^{(n+1)})}$ --
                Ukážeme nasledovne:
                %%% {{{
                 \begin{itemize}
                    \item[a] $ \highlightdim{(\forall x) (X \implies
                        Y)} \provable 
                            (\forall x) (X \implies Y)$ -- predpoklad
                            je vždy dokázateľný
                    \item[b] $ \provable \highlightdim{
                        (\forall x) (X \implies Y)}
                                \implies (X \implies Y)$ -- axióma
                                špecifikácie
                    \item[c] $ \highlightdim{(\forall x) (X \implies
                        Y)} \provable
                            X \implies Y$ -- MP a,b
                    \item[d] $ \highlightdim{(\forall x) (X \implies
                        Y)} \provable
                            (\forall x) X \implies (\forall x) Y$ --
                            pravidlo zavedenia všeobecného
                            kvantifikátora aplikované na c
                    \item[e] $ \provable \highlightdim{(\forall x) (X
                                \implies Y)}
                        \implies
                            ((\forall x) X \implies (\forall x) Y)$ --
                            veta o dedukcii v predikátovej logike.%
                            \footnote{Pozor, treba si riadne
                                premyslieť, že ju môžeme použiť. Totiž, v
                                dôkaze d sme nikne nepoužili pravidlo
                                zovšeobecnenia na premennú, ktorá by bola
                                voľná v $(\forall x) (X \implies Y)$ --
                                použili sme to iba na premennú $x$ a tá je
                                viazaná.
                            }
                 \end{itemize}
                 %%% }}}

            \item[5] $\provable \highlightc{(\forall y) B} \implies 
                \highlightb{((\forall y)
                    (B \implies P^{(n+1)}) \implies
                    (\forall y) P^{(n+1)})}$ -- pravidlo jednoduchého sylogizmu
                    aplikované na x,y

            \item[z] $\provable 
                \forallxton \left[
                \highlightc{(\forall y) B} \implies 
                \highlightb{((\forall y)
                    (B \implies P^{(n+1)}) \implies
                    (\forall y) P^{(n+1)})}
                \right] $ -- $n$-krát aplikované pravidlo zovšeobecnenia
                 na krok 5

            \item[6] $\provable \highlighta{\existsxton} 
                    \highlightc{(\forall y) B} \implies
                    \highlighta{\existsxton} \left[
                        \highlightb{
                        (\forall y) (B \implies P^{(n+1)})
                        \implies (\forall y) P^{(n+1)}) } \right]$ --
                $n$-krát použijeme
                    $\provable (\forall x)(A \implies B) \implies
                     ((\exists x) A \implies (\exists x)B)$, čo sa dá
                     dokázať nasledovne:
                     %%% {{{
                   \begin{itemize}
                    \item[c] $ \highlightdim{
                        (\forall x) (X \implies Y)}
                                \provable X \implies Y$ -- už sme
                                mali

                    \item[j] $ \provable Y \implies (\exists x) Y$ --
                        duálny tvar axiómy špecifikácie

                    \item[k] $ \highlightdim{
                        (\forall x) (X \implies Y)} \provable
                            X \implies (\exists x) Y$ -- JS c,j

                    \item[l] $ \highlightdim{
                        (\forall x) (X \implies Y)} \provable
                            (\exists x) X \implies (\exists x) Y$ --
                            pravidlo zavedenia existenčného
                            kvantifikátora, $x$ nie je voľné v
                            $(\exists x) Y$.

                    \item[m] $ \provable \highlightdim{
                        (\forall x) (X \implies Y)} \implies
                            (\exists x) X \implies (\exists x) Y$ --
                            Veta o dedukcii, čitateľ si môže
                            premyslieť, že ju môžeme použiť
                   
                   \end{itemize}
                   %%% }}}

            \item[7] $\provable
                 \highlighta{\existsxton} \left[
                 \highlightb{(\forall y) (B \implies P^{(n+1)})
                 \implies (\forall y) P^{(n+1)}} \right]$ -- MP
                 indukčného predpokladu a 6
            \end{itemize}
        %%% }}}

        \medskip
        \item[$\Leftarrow$]
        Predpokladáme, že je dokázateľné $\provable A^* : 
                \existsxton [(\forall y) (B \implies P^{(n+1)}) 
                \implies (\forall y) P^{(n+1)}]$.
        Treba si uvedomiť,
        že na predikát $P^{(n+1)}$ nekladieme žiadne nároky a teda je
        to dokázateľné pre ľubovoľný taký predikát. No ale
        formula $B$ sa dá chápať ako špeciálny prípad $(n+1)$-árneho
        predikátu. Preto bude dokázateľná aj inštancia
        formuly $A^*$, ktorá vyzerá nasledovne:
        $\provable  \existsxton [(\forall y) (B \implies B) 
            \implies (\forall y) B]$

        %%% {{{ <==
            \begin{itemize}
            \item[1] $\provable \highlightc{
                \existsxton [(\forall y) (B \implies B) 
                \implies (\forall y) B]}$

            \item[2] $\provable (\exists x) (X \implies Y) \implies
                ((\forall x) X \implies (\exists x) Y)$ -- dá sa
                dokázať napríklad takto:
                %%% {{{
                \begin{itemize}
                \item $\provable X \implies (\neg Y \implies \neg (X
                        \implies Y))$

                \item $\provable (\forall x) X \implies (\forall x)
                (\neg Y
                   \implies \neg (X \implies Y))$ -- veta o zavedení
                   všeobecných kvantifikátorov

                \item $(\forall x) X \provable
                    (\forall x) (\neg Y \implies \neg (X \implies Y))$
                    -- veta o dedukcii

                \item $(\forall x) X \provable
                    \highlighta{(\forall x) \neg Y} \implies
                    \highlightb{(\forall x) \neg (X \implies Y)}$ --
                    veta o distribúcii kvantifikátorov\footnote{
                        formálne by sme mali ešte spraviť medzikrok
                        $(\forall x) X \provable \neg Y \implies
                                \neg (X \implies Y)$
                    }

                \item $(\forall x) X \provable
                    \highlightb{\highlightc{\neg} (\forall x) 
                                 \neg (X \implies Y)} \implies
                    \highlighta{\highlightc{\neg} (\forall x) 
                                 \neg Y}$ -- obmena implikácie

                \item $\highlighta{(\forall x)} X \provable
                    \highlightb{\highlightp{(\exists x)} (X \implies
                    Y)} \implies
                    \highlightp{(\exists x)} Y$ -- nahradenie
                    kvantifikátorov

                \item $\provable \highlightb{(\exists x) (X \implies Y)} 
                    \implies
                     \highlighta{(\forall x) X } \implies
                    (\exists x) Y$ -- 2 krát veta o dedukcii
                \end{itemize}
                %%% }}}
            \item[3] $\provable \highlightc{
                \existsxton [(\forall y) (B \implies B) 
                \implies  (\forall y) B]} \implies $ \\
                \phantom{x}$\quad\quad
                \highlighta{
                [ \forallxton (\forall y) (B \implies B)
                \implies \existsxton (\forall y) B]}$ -- $n$-krát
                využijeme 2 nasledujúcim štýlom:
                Použijeme na dané pravidlo vetu o zavedení
                existenčného kvantifikátora. Následne, pravú stranu
                hlavnej implikácie vidíme ako kandidáta na krok 2.
                Preto ju na novom riadku rozpíšeme podľa tohoto pravidla
                a následne použítím jednoduchého sylogizmu tieto 2
                riadky zložíme. Tím dostaneme variantu 2 s pridanou
                ďalšou premennou a toto opakujeme príslušný počet
                krát.

            \item[4] $\provable \highlighta{
                \highlighto{\forallxton (\forall y) (B \implies B)}
                \implies \highlightp{\existsxton (\forall y) B}}$.
                -- MP 1,3
            \item[5]
                $\provable \highlighto{\forallxton (\forall y) (B
                \implies B)}$
                -- $(n+1)$-krát pravidlo zovšeobecnenia použité na 
                dokázateľnú formulu $\provable B \implies B$.
            \item[6]
                $\provable \highlightp{\existsxton (\forall y) B}$
                -- MP 4,5
            \end{itemize}
        %%% }}}
        \end{itemize}
        %%% }}}

        Ešte potrebujeme transformovať formulu $A^*$ na formulu s
        hodnosťou $m-1$. Vieme, že $B$ je v prenexnom tvare
        (predpokladami sme to hneď na začiatku) a teda ju môžeme
        zapísať ako 
        $B:(Q_1 z_1)(Q_2 z_2) \dots (Q_l z_l) C$, kde $C$ je formula
        bez kvantifikátorov. Vieme, že hodnosť $B$, resp.
        hodnosť jej prefixu $(Q_1 z_1)(Q_2 z_2) \dots (Q_l z_l)$ je $m-1$
        nakoľko hodnosť $A$ je $m$ a v $A$ sa pred $B$ nachádza
        jeden všeobecný kvantifikátor.
        %%% {{{
        \begin{itemize}
        %%% pomocne makra
        \def\lefta{\scalebox{3}[1]{\highlighta{[}} }
        \def\leftb{\scalebox{3}[1]{\highlightb{[}} }
        \def\righta{\scalebox{3}[1]{\highlighta{]}} }
        \def\rightb{\scalebox{3}[1]{\highlightb{]}} }

        \item[$A^*$] 
        $=\highlightdim{\existsxton} 
            \lefta (\forall y)
            \leftb
              (Q_1 z_1) (Q_2 z_2) \dots (Q_l z_l) C \implies
              P^{(n+1)} \rightb \implies (\forall y)
              P^{(n+1)} \righta$

        \item[] $\Leftrightarrow$
        $ \highlightdim{\existsxton} \lefta
                    (\forall y) (\overline{Q_1} z_1)
                    (\overline{Q_2} z_2) \dots
                    (\overline{Q_l} z_l) \leftb
                        C \implies P^{(n+1)} \rightb
                            \implies (\forall u)
                                P^{(n+1)} \righta$ -- veta o variantoch
                                (druhé $y$ premenované na $u$)
                                + $l$ prenexných operácií d)
        \item[] $\Leftrightarrow$
        $ \highlightdim{\existsxton} \highlightc{(\exists y)}
                \lefta
                    (\overline{Q_1} z_1)
                    (\overline{Q_2} z_2) \dots
                    (\overline{Q_l} z_l) \leftb
                        C \implies P^{(n+1)} \rightb
                            \implies (\forall u)
                                P^{(n+1)} \righta$ -- prenexná
                                operácia d) aplikovaná na $y$
        \item[] $\Leftrightarrow$
        $ \highlightdim{\existsxton} (\exists y)
                    (Q_1 z_1)
                    (Q_2 z_2) \dots
                    (Q_l z_l) \lefta \leftb
                        C \implies P^{(n+1)} \rightb
                            \implies (\forall u)
                                P^{(n+1)} \righta$ -- $l$-krát prenexná
                                operácia d)

        \item[] $\Leftrightarrow$
        $ \highlightdim{\existsxton} (\exists y)
                    (Q_1 z_1)
                    (Q_2 z_2) \dots
                    (Q_l z_l) (\forall u) \lefta \leftb
                        C \implies P^{(n+1)} \rightb
                            \implies
                                P^{(n+1)} \righta$ -- prenexná
                                operácia c) aplikovaná na $u$

            %%% zmaz pomocne makra
            \let\lefta\undefined
            \let\leftb\undefined
            \let\righta\undefined
            \let\rightb\undefined
        \end{itemize}
        %%% }}}
        Posledná formula má hodnosť $m-1$ a je v prenexnom tvare.
        Tým pádom ju vieme podľa
        indukčného predpokladu previesť na Skolemov normálny tvar.
    \end{itemize}
%%% }}}    
\end{dokaz}
